app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(app2(minus, x), 0) -> x
app2(app2(minus, app2(s, x)), app2(s, y)) -> app2(app2(minus, x), y)
app2(app2(div, 0), app2(s, y)) -> 0
app2(app2(div, app2(s, x)), app2(s, y)) -> app2(s, app2(app2(div, app2(app2(minus, x), y)), app2(s, y)))
↳ QTRS
↳ Non-Overlap Check
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(app2(minus, x), 0) -> x
app2(app2(minus, app2(s, x)), app2(s, y)) -> app2(app2(minus, x), y)
app2(app2(div, 0), app2(s, y)) -> 0
app2(app2(div, app2(s, x)), app2(s, y)) -> app2(s, app2(app2(div, app2(app2(minus, x), y)), app2(s, y)))
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(app2(minus, x), 0) -> x
app2(app2(minus, app2(s, x)), app2(s, y)) -> app2(app2(minus, x), y)
app2(app2(div, 0), app2(s, y)) -> 0
app2(app2(div, app2(s, x)), app2(s, y)) -> app2(s, app2(app2(div, app2(app2(minus, x), y)), app2(s, y)))
app2(app2(map, x0), nil)
app2(app2(map, x0), app2(app2(cons, x1), x2))
app2(app2(minus, x0), 0)
app2(app2(minus, app2(s, x0)), app2(s, x1))
app2(app2(div, 0), app2(s, x0))
app2(app2(div, app2(s, x0)), app2(s, x1))
APP2(app2(minus, app2(s, x)), app2(s, y)) -> APP2(minus, x)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(f, x)
APP2(app2(div, app2(s, x)), app2(s, y)) -> APP2(div, app2(app2(minus, x), y))
APP2(app2(minus, app2(s, x)), app2(s, y)) -> APP2(app2(minus, x), y)
APP2(app2(div, app2(s, x)), app2(s, y)) -> APP2(app2(div, app2(app2(minus, x), y)), app2(s, y))
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(map, f), xs)
APP2(app2(div, app2(s, x)), app2(s, y)) -> APP2(minus, x)
APP2(app2(div, app2(s, x)), app2(s, y)) -> APP2(app2(minus, x), y)
APP2(app2(div, app2(s, x)), app2(s, y)) -> APP2(s, app2(app2(div, app2(app2(minus, x), y)), app2(s, y)))
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(cons, app2(f, x))
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(app2(minus, x), 0) -> x
app2(app2(minus, app2(s, x)), app2(s, y)) -> app2(app2(minus, x), y)
app2(app2(div, 0), app2(s, y)) -> 0
app2(app2(div, app2(s, x)), app2(s, y)) -> app2(s, app2(app2(div, app2(app2(minus, x), y)), app2(s, y)))
app2(app2(map, x0), nil)
app2(app2(map, x0), app2(app2(cons, x1), x2))
app2(app2(minus, x0), 0)
app2(app2(minus, app2(s, x0)), app2(s, x1))
app2(app2(div, 0), app2(s, x0))
app2(app2(div, app2(s, x0)), app2(s, x1))
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
APP2(app2(minus, app2(s, x)), app2(s, y)) -> APP2(minus, x)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(f, x)
APP2(app2(div, app2(s, x)), app2(s, y)) -> APP2(div, app2(app2(minus, x), y))
APP2(app2(minus, app2(s, x)), app2(s, y)) -> APP2(app2(minus, x), y)
APP2(app2(div, app2(s, x)), app2(s, y)) -> APP2(app2(div, app2(app2(minus, x), y)), app2(s, y))
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(map, f), xs)
APP2(app2(div, app2(s, x)), app2(s, y)) -> APP2(minus, x)
APP2(app2(div, app2(s, x)), app2(s, y)) -> APP2(app2(minus, x), y)
APP2(app2(div, app2(s, x)), app2(s, y)) -> APP2(s, app2(app2(div, app2(app2(minus, x), y)), app2(s, y)))
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(cons, app2(f, x))
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(app2(minus, x), 0) -> x
app2(app2(minus, app2(s, x)), app2(s, y)) -> app2(app2(minus, x), y)
app2(app2(div, 0), app2(s, y)) -> 0
app2(app2(div, app2(s, x)), app2(s, y)) -> app2(s, app2(app2(div, app2(app2(minus, x), y)), app2(s, y)))
app2(app2(map, x0), nil)
app2(app2(map, x0), app2(app2(cons, x1), x2))
app2(app2(minus, x0), 0)
app2(app2(minus, app2(s, x0)), app2(s, x1))
app2(app2(div, 0), app2(s, x0))
app2(app2(div, app2(s, x0)), app2(s, x1))
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
APP2(app2(minus, app2(s, x)), app2(s, y)) -> APP2(app2(minus, x), y)
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(app2(minus, x), 0) -> x
app2(app2(minus, app2(s, x)), app2(s, y)) -> app2(app2(minus, x), y)
app2(app2(div, 0), app2(s, y)) -> 0
app2(app2(div, app2(s, x)), app2(s, y)) -> app2(s, app2(app2(div, app2(app2(minus, x), y)), app2(s, y)))
app2(app2(map, x0), nil)
app2(app2(map, x0), app2(app2(cons, x1), x2))
app2(app2(minus, x0), 0)
app2(app2(minus, app2(s, x0)), app2(s, x1))
app2(app2(div, 0), app2(s, x0))
app2(app2(div, app2(s, x0)), app2(s, x1))
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
APP2(app2(minus, app2(s, x)), app2(s, y)) -> APP2(app2(minus, x), y)
APP1 > app1
APP1 > minus
s > app1
s > minus
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(app2(minus, x), 0) -> x
app2(app2(minus, app2(s, x)), app2(s, y)) -> app2(app2(minus, x), y)
app2(app2(div, 0), app2(s, y)) -> 0
app2(app2(div, app2(s, x)), app2(s, y)) -> app2(s, app2(app2(div, app2(app2(minus, x), y)), app2(s, y)))
app2(app2(map, x0), nil)
app2(app2(map, x0), app2(app2(cons, x1), x2))
app2(app2(minus, x0), 0)
app2(app2(minus, app2(s, x0)), app2(s, x1))
app2(app2(div, 0), app2(s, x0))
app2(app2(div, app2(s, x0)), app2(s, x1))
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
APP2(app2(div, app2(s, x)), app2(s, y)) -> APP2(app2(div, app2(app2(minus, x), y)), app2(s, y))
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(app2(minus, x), 0) -> x
app2(app2(minus, app2(s, x)), app2(s, y)) -> app2(app2(minus, x), y)
app2(app2(div, 0), app2(s, y)) -> 0
app2(app2(div, app2(s, x)), app2(s, y)) -> app2(s, app2(app2(div, app2(app2(minus, x), y)), app2(s, y)))
app2(app2(map, x0), nil)
app2(app2(map, x0), app2(app2(cons, x1), x2))
app2(app2(minus, x0), 0)
app2(app2(minus, app2(s, x0)), app2(s, x1))
app2(app2(div, 0), app2(s, x0))
app2(app2(div, app2(s, x0)), app2(s, x1))
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(f, x)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(map, f), xs)
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(app2(minus, x), 0) -> x
app2(app2(minus, app2(s, x)), app2(s, y)) -> app2(app2(minus, x), y)
app2(app2(div, 0), app2(s, y)) -> 0
app2(app2(div, app2(s, x)), app2(s, y)) -> app2(s, app2(app2(div, app2(app2(minus, x), y)), app2(s, y)))
app2(app2(map, x0), nil)
app2(app2(map, x0), app2(app2(cons, x1), x2))
app2(app2(minus, x0), 0)
app2(app2(minus, app2(s, x0)), app2(s, x1))
app2(app2(div, 0), app2(s, x0))
app2(app2(div, app2(s, x0)), app2(s, x1))
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(f, x)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(map, f), xs)
app2 > map
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(app2(minus, x), 0) -> x
app2(app2(minus, app2(s, x)), app2(s, y)) -> app2(app2(minus, x), y)
app2(app2(div, 0), app2(s, y)) -> 0
app2(app2(div, app2(s, x)), app2(s, y)) -> app2(s, app2(app2(div, app2(app2(minus, x), y)), app2(s, y)))
app2(app2(map, x0), nil)
app2(app2(map, x0), app2(app2(cons, x1), x2))
app2(app2(minus, x0), 0)
app2(app2(minus, app2(s, x0)), app2(s, x1))
app2(app2(div, 0), app2(s, x0))
app2(app2(div, app2(s, x0)), app2(s, x1))